Nuprl Lemma : ma-single-sframe-feasible
0,22
postcript
pdf
l
:IdLnk,
tg
:Id,
L
:Knd List. Feasible(only
L
sends on (
l
with
tg
))
latex
Definitions
t
T
,
False
,
P
Q
,
x
:
A
.
B
(
x
)
,
P
&
Q
,
b
,
f
(
x
)
,
x
dom(
f
)
,
x
dom(
f
).
v
=
f
(
x
)
P
(
x
;
v
)
,
mk-ma
,
x
:
v
,
,
f
(
x
)?
z
,
Feasible(
M
)
,
only
L
sends on (
l
with
tg
)
Lemmas
IdLnk
wf
,
Id
wf
,
false
wf
,
Knd
wf
origin
l:IdLnk, tg:Id, L:Knd List. Feasible(only L sends on (l with tg)) l:IdLnk, tg:Id, L:Knd List. Feasible(only L sends on (l with tg)) 
T
Qx:A. B(x)
b dom(f)xdom(f). v=f(x) P(x;v)